Nuprl Lemma : fpf-trivial-subtype-set
11,40
postcript
pdf
A
:Type,
P
:(
A
),
f
:
a
:{
a
:
A
|
P
(
a
)} fp
:Type
Top.
f
a
:
A
fp
:Type
Top
latex
Definitions
x
.
t
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
,
t
T
Lemmas
strong-subtype-self
,
strong-subtype-set3
,
subtype-fpf3
,
fpf
wf
origin
A:Type, P:(A
), f:a:{a:A| P(a)} fp :Type 
Top. f 
a:A fp :Type Top A:Type, P:(A), f:a:{a:A| P(a)} fp :Type Top. f a:A fp :Type Top 
x. t(x)
Qx:A. B(x) T